(set-logic QF_RDL)
(set-info :source |
Source unknown
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun cvclZero () Real)
(declare-fun x_0 () Bool)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Real)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Bool)
(declare-fun x_27 () Real)
(declare-fun x_28 () Bool)
(declare-fun x_29 () Bool)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(assert (let ((?v_19 (not x_25)) (?v_20 (not x_26))) (let ((?v_21 (and ?v_19 ?v_20)) (?v_57 (not x_28)) (?v_58 (not x_29))) (let ((?v_59 (and ?v_57 ?v_58)) (?v_42 (not x_30)) (?v_43 (not x_31))) (let ((?v_45 (and ?v_42 ?v_43)) (?v_24 (and (= x_28 x_14) (= x_29 x_15))) (?v_54 (not x_14)) (?v_52 (not x_15))) (let ((?v_49 (and ?v_54 ?v_52)) (?v_13 (and (= x_25 x_11) (= x_26 x_12))) (?v_38 (not x_16)) (?v_35 (not x_17))) (let ((?v_30 (and ?v_38 ?v_35)) (?v_55 (and ?v_54 x_15)) (?v_22 (and (= x_30 x_16) (= x_31 x_17))) (?v_40 (and ?v_38 x_17)) (?v_16 (not x_11)) (?v_14 (not x_12))) (let ((?v_9 (and ?v_16 ?v_14)) (?v_17 (and ?v_16 x_12)) (?v_81 (and (= x_14 x_4) (= x_15 x_5))) (?v_107 (not x_4)) (?v_105 (not x_5))) (let ((?v_101 (and ?v_107 ?v_105)) (?v_73 (and (= x_11 x_0) (= x_12 x_1))) (?v_95 (not x_2)) (?v_92 (not x_3))) (let ((?v_85 (and ?v_95 ?v_92)) (?v_108 (and ?v_107 x_5)) (?v_79 (and (= x_16 x_2) (= x_17 x_3))) (?v_97 (and ?v_95 x_3)) (?v_76 (not x_0)) (?v_74 (not x_1))) (let ((?v_66 (and ?v_76 ?v_74)) (?v_77 (and ?v_76 x_1)) (?v_67 (- cvclZero x_6))) (let ((?v_63 (< ?v_67 0)) (?v_86 (- cvclZero x_7))) (let ((?v_62 (< ?v_86 0)) (?v_102 (- cvclZero x_8))) (let ((?v_61 (< ?v_102 0)) (?v_0 (- x_9 cvclZero))) (let ((?v_68 (= ?v_0 0)) (?v_3 (< (- x_18 x_19) 0))) (let ((?v_4 (ite ?v_3 (< (- x_18 x_20) 0) (< (- x_19 x_20) 0))) (?v_47 (= (- x_34 x_20) 0)) (?v_23 (= (- x_33 x_19) 0)) (?v_25 (= (- x_32 x_18) 0)) (?v_7 (= (- x_27 x_13) 0)) (?v_8 (- x_24 cvclZero))) (let ((?v_27 (= ?v_8 0)) (?v_6 (- x_22 x_20))) (let ((?v_10 (= ?v_6 0)) (?v_1 (- x_13 cvclZero))) (let ((?v_11 (= ?v_1 0)) (?v_15 (- x_22 x_34))) (let ((?v_12 (< ?v_15 0)) (?v_29 (= ?v_8 1)) (?v_32 (not ?v_11)) (?v_34 (= ?v_8 2)) (?v_2 (- x_27 cvclZero))) (let ((?v_110 (= ?v_2 1)) (?v_37 (= ?v_8 3)) (?v_18 (= ?v_1 1)) (?v_39 (= ?v_8 4))) (let ((?v_113 (not ?v_18)) (?v_44 (= ?v_8 5)) (?v_46 (= ?v_2 0)) (?v_28 (- x_22 x_19))) (let ((?v_31 (= ?v_28 0)) (?v_36 (- x_22 x_33))) (let ((?v_33 (< ?v_36 0)) (?v_111 (= ?v_2 2)) (?v_41 (= ?v_1 2))) (let ((?v_114 (not ?v_41)) (?v_48 (- x_22 x_18))) (let ((?v_50 (= ?v_48 0)) (?v_53 (- x_22 x_32))) (let ((?v_51 (< ?v_53 0)) (?v_112 (= ?v_2 3)) (?v_56 (= ?v_1 3))) (let ((?v_115 (not ?v_56)) (?v_60 (< (- x_8 x_7) 0))) (let ((?v_64 (ite ?v_60 (< (- x_8 x_6) 0) (< (- x_7 x_6) 0))) (?v_100 (= (- x_20 x_6) 0)) (?v_80 (= (- x_19 x_7) 0)) (?v_82 (= (- x_18 x_8) 0)) (?v_69 (= (- x_13 x_9) 0)) (?v_70 (- x_10 cvclZero))) (let ((?v_84 (= ?v_70 0)) (?v_71 (= ?v_67 0)) (?v_75 (- cvclZero x_20))) (let ((?v_72 (< ?v_75 0)) (?v_87 (= ?v_70 1)) (?v_89 (not ?v_68)) (?v_91 (= ?v_70 2)) (?v_94 (= ?v_70 3)) (?v_78 (= ?v_0 1)) (?v_96 (= ?v_70 4))) (let ((?v_116 (not ?v_78)) (?v_99 (= ?v_70 5)) (?v_88 (= ?v_86 0)) (?v_93 (- cvclZero x_19))) (let ((?v_90 (< ?v_93 0)) (?v_98 (= ?v_0 2))) (let ((?v_117 (not ?v_98)) (?v_103 (= ?v_102 0)) (?v_106 (- cvclZero x_18))) (let ((?v_104 (< ?v_106 0)) (?v_109 (= ?v_0 3))) (let ((?v_118 (not ?v_109)) (?v_5 (- x_35 cvclZero)) (?v_26 (- x_37 cvclZero)) (?v_65 (- x_21 cvclZero)) (?v_83 (- x_23 cvclZero))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (< ?v_0 0)) (<= ?v_0 3)) (not (< ?v_1 0))) (<= ?v_1 3)) (not (< ?v_2 0))) (<= ?v_2 3)) ?v_66) ?v_85) ?v_101) ?v_63) ?v_62) ?v_61) ?v_68) (or (and (and (and (and (and (and (and (and (and (= ?v_5 0) (ite ?v_4 (ite ?v_3 (< ?v_48 0) (< ?v_28 0)) (< ?v_6 0))) (ite ?v_4 (ite ?v_3 (= (- x_36 x_18) 0) (= (- x_36 x_19) 0)) (= (- x_36 x_20) 0))) ?v_13) ?v_22) ?v_24) ?v_47) ?v_23) ?v_25) ?v_7) (and (and (= ?v_5 1) (or (or (and (and (and (and (and (= ?v_26 1) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_27 ?v_9) ?v_10) ?v_11) x_25) ?v_20) ?v_12) (<= (- x_34 x_22) 2)) ?v_7) (and (and (and (and (and (and ?v_29 ?v_9) ?v_10) ?v_32) ?v_12) ?v_7) ?v_13)) (and (and (and (and (and (and (and ?v_34 x_11) ?v_14) ?v_10) ?v_19) x_26) ?v_110) (<= ?v_15 (- 4)))) (and (and (and (and (and (and (and ?v_37 ?v_17) ?v_10) ?v_18) x_25) x_26) ?v_12) ?v_7)) (and (and (and (and (and (and ?v_39 ?v_17) ?v_10) ?v_113) ?v_21) ?v_12) ?v_7)) (and (and (and (and (and (and ?v_44 x_11) x_12) ?v_10) ?v_21) ?v_46) ?v_12))) ?v_22) ?v_23) ?v_24) ?v_25) (and (and (and (and (and (= ?v_26 2) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_27 ?v_30) ?v_31) ?v_11) x_30) ?v_43) ?v_33) (<= (- x_33 x_22) 2)) ?v_7) (and (and (and (and (and (and ?v_29 ?v_30) ?v_31) ?v_32) ?v_33) ?v_7) ?v_22)) (and (and (and (and (and (and (and ?v_34 x_16) ?v_35) ?v_31) ?v_42) x_31) ?v_111) (<= ?v_36 (- 4)))) (and (and (and (and (and (and (and ?v_37 ?v_40) ?v_31) ?v_41) x_30) x_31) ?v_33) ?v_7)) (and (and (and (and (and (and ?v_39 ?v_40) ?v_31) ?v_114) ?v_45) ?v_33) ?v_7)) (and (and (and (and (and (and ?v_44 x_16) x_17) ?v_31) ?v_45) ?v_46) ?v_33))) ?v_13) ?v_47) ?v_24) ?v_25)) (and (and (and (and (and (= ?v_26 3) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_27 ?v_49) ?v_50) ?v_11) x_28) ?v_58) ?v_51) (<= (- x_32 x_22) 2)) ?v_7) (and (and (and (and (and (and ?v_29 ?v_49) ?v_50) ?v_32) ?v_51) ?v_7) ?v_24)) (and (and (and (and (and (and (and ?v_34 x_14) ?v_52) ?v_50) ?v_57) x_29) ?v_112) (<= ?v_53 (- 4)))) (and (and (and (and (and (and (and ?v_37 ?v_55) ?v_50) ?v_56) x_28) x_29) ?v_51) ?v_7)) (and (and (and (and (and (and ?v_39 ?v_55) ?v_50) ?v_115) ?v_59) ?v_51) ?v_7)) (and (and (and (and (and (and ?v_44 x_14) x_15) ?v_50) ?v_59) ?v_46) ?v_51))) ?v_13) ?v_47) ?v_22) ?v_23))) (= (- x_36 x_22) 0)))) (or (and (and (and (and (and (and (and (and (and (= ?v_65 0) (ite ?v_64 (ite ?v_60 ?v_61 ?v_62) ?v_63)) (ite ?v_64 (ite ?v_60 (= (- x_22 x_8) 0) (= (- x_22 x_7) 0)) (= (- x_22 x_6) 0))) ?v_73) ?v_79) ?v_81) ?v_100) ?v_80) ?v_82) ?v_69) (and (and (= ?v_65 1) (or (or (and (and (and (and (and (= ?v_83 1) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_84 ?v_66) ?v_71) ?v_68) x_11) ?v_14) ?v_72) (<= (- x_20 cvclZero) 2)) ?v_69) (and (and (and (and (and (and ?v_87 ?v_66) ?v_71) ?v_89) ?v_72) ?v_69) ?v_73)) (and (and (and (and (and (and (and ?v_91 x_0) ?v_74) ?v_71) ?v_16) x_12) ?v_18) (<= ?v_75 (- 4)))) (and (and (and (and (and (and (and ?v_94 ?v_77) ?v_71) ?v_78) x_11) x_12) ?v_72) ?v_69)) (and (and (and (and (and (and ?v_96 ?v_77) ?v_71) ?v_116) ?v_9) ?v_72) ?v_69)) (and (and (and (and (and (and ?v_99 x_0) x_1) ?v_71) ?v_9) ?v_11) ?v_72))) ?v_79) ?v_80) ?v_81) ?v_82) (and (and (and (and (and (= ?v_83 2) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_84 ?v_85) ?v_88) ?v_68) x_16) ?v_35) ?v_90) (<= (- x_19 cvclZero) 2)) ?v_69) (and (and (and (and (and (and ?v_87 ?v_85) ?v_88) ?v_89) ?v_90) ?v_69) ?v_79)) (and (and (and (and (and (and (and ?v_91 x_2) ?v_92) ?v_88) ?v_38) x_17) ?v_41) (<= ?v_93 (- 4)))) (and (and (and (and (and (and (and ?v_94 ?v_97) ?v_88) ?v_98) x_16) x_17) ?v_90) ?v_69)) (and (and (and (and (and (and ?v_96 ?v_97) ?v_88) ?v_117) ?v_30) ?v_90) ?v_69)) (and (and (and (and (and (and ?v_99 x_2) x_3) ?v_88) ?v_30) ?v_11) ?v_90))) ?v_73) ?v_100) ?v_81) ?v_82)) (and (and (and (and (and (= ?v_83 3) (or (or (or (or (or (and (and (and (and (and (and (and (and ?v_84 ?v_101) ?v_103) ?v_68) x_14) ?v_52) ?v_104) (<= (- x_18 cvclZero) 2)) ?v_69) (and (and (and (and (and (and ?v_87 ?v_101) ?v_103) ?v_89) ?v_104) ?v_69) ?v_81)) (and (and (and (and (and (and (and ?v_91 x_4) ?v_105) ?v_103) ?v_54) x_15) ?v_56) (<= ?v_106 (- 4)))) (and (and (and (and (and (and (and ?v_94 ?v_108) ?v_103) ?v_109) x_14) x_15) ?v_104) ?v_69)) (and (and (and (and (and (and ?v_96 ?v_108) ?v_103) ?v_118) ?v_49) ?v_104) ?v_69)) (and (and (and (and (and (and ?v_99 x_4) x_5) ?v_103) ?v_49) ?v_11) ?v_104))) ?v_73) ?v_100) ?v_79) ?v_80))) (= (- x_22 cvclZero) 0)))) (or (or (or (or (or (or (or (or (and (and x_25 x_26) (not ?v_110)) (and (and x_30 x_31) (not ?v_111))) (and (and x_28 x_29) (not ?v_112))) (and (and x_11 x_12) ?v_113)) (and (and x_16 x_17) ?v_114)) (and (and x_14 x_15) ?v_115)) (and (and x_0 x_1) ?v_116)) (and (and x_2 x_3) ?v_117)) (and (and x_4 x_5) ?v_118)))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
